\begin{tabbing}
$\forall$\=${\it es}$:ES, $T$, $A$:Type, $l$:IdLnk, ${\it tg}$, $a$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow\mathbb{B}$),\+
\\[0ex]$f$:(\{$s$:State(${\it ds}$)$\mid$ $\uparrow$($P$($s$))\} $\rightarrow$$A$$\rightarrow$$T$).
\-\\[0ex]weak{-}precond{-}send{-}p(${\it es}$;$T$;$A$;$l$;${\it tg}$;$a$;${\it ds}$;$P$;$f$) $\in$ $\mathbb{P}$
\end{tabbing}